J:. 1  n < J+1. (1/n * n)  2 - (1/J) 

latex

Definitions

i  j < k, {i..j}, False, A  B, P  Q, p  q, <+*>, 0, r+gp, e, i <z j, Y, (op,id) lb  i < ub. E(i),  lb  i < ub. E(i), (r) i  k < j. E(k), 1/r, r * s, qpositive(r), p q, q_le(r;s), <+>, t.2, t.1, , x f y, a  b, ff, (i = j), tt, if b then t else f fi , qeq(r;s), b, P & Q, A, x. t(x), True, T, P  Q, r + s, P  Q, r - s, (r/s), a  j < b. E(j), r  s, {T}, SQType(T), , P  Q, t  T, x:A. B(x), x(s), Dec(P), , S  T

Lemmas

le wf, int-rational, qle transitivity qorder, qle-int, qadd-add, qmul-qdiv-cancel4, qmul assoc, qmul com, qmul ac 1 qrng, qmul one qrng, qmul-positive, qmul-mul, qless-int, qless wf, qmul-qdiv-cancel, qmul over minus qrng, qmul over plus qrng, qmul preserves qle, mon ident q, qadd inv assoc q, qinverse q, mon assoc q, qadd com, qmul wf, qadd ac 1 q, qadd wf, qsum wf, qadd preserves qle, int entire, false wf, assert-qeq, qeq wf2, assert wf, qsub wf, int seg wf, int-eq-in-rationals, not functionality wrt iff, int inc rationals, qdiv wf, sum unroll hi q, rationals wf, true wf, squash wf, qle wf, nat plus wf, decidable int equal, nat plus properties